Search Results

Documents authored by Chakraborty, Supratik

Document
DOI: 10.4230/LIPIcs.MFCS.2022.30
On Synthesizing Computable Skolem Functions for First Order Logic

Authors: Supratik Chakraborty and S. Akshay

Published in: LIPIcs, Volume 241, 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)

Abstract
Skolem functions play a central role in the study of first order logic, both from theoretical and practical perspectives. While every Skolemized formula in first-order logic makes use of Skolem constants and/or functions, not all such Skolem constants and/or functions admit effectively computable interpretations. Indeed, the question of whether there exists an effectively computable interpretation of a Skolem function, and if so, how to automatically synthesize it, is fundamental to their use in several applications, such as planning, strategy synthesis, program synthesis etc. In this paper, we investigate the computability of Skolem functions and their automated synthesis in the full generality of first order logic. We first show a strong negative result, that even under mild assumptions on the vocabulary, it is impossible to obtain computable interpretations of Skolem functions. We then show a positive result, providing a precise characterization of first-order theories that admit effective interpretations of Skolem functions, and also present algorithms to automatically synthesize such interpretations. We discuss applications of our characterization as well as complexity bounds for Skolem functions (interpreted as Turing machines).
Cite as

Supratik Chakraborty and S. Akshay. On Synthesizing Computable Skolem Functions for First Order Logic. In 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 241, pp. 30:1-30:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{chakraborty_et_al:LIPIcs.MFCS.2022.30,
  author =	{Chakraborty, Supratik and Akshay, S.},
  title =	{{On Synthesizing Computable Skolem Functions for First Order Logic}},
  booktitle =	{47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)},
  pages =	{30:1--30:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-256-3},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{241},
  editor =	{Szeider, Stefan and Ganian, Robert and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2022.30},
  URN =		{urn:nbn:de:0030-drops-168285},
  doi =		{10.4230/LIPIcs.MFCS.2022.30},
  annote =	{Keywords: Skolem functions, Automated, Synthesis, First order logic, Computability}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2017.40
On Petri Nets with Hierarchical Special Arcs

Authors: S. Akshay, Supratik Chakraborty, Ankush Das, Vishal Jagannath, and Sai Sandeep

Published in: LIPIcs, Volume 85, 28th International Conference on Concurrency Theory (CONCUR 2017)

Abstract
We investigate the decidability of termination, reachability, coverability and deadlock-freeness of Petri nets endowed with a hierarchy of places, and with inhibitor arcs, reset arcs and transfer arcs that respect this hierarchy. We also investigate what happens when we have a mix of these special arcs, some of which respect the hierarchy, while others do not. We settle the decidability status of the above four problems for all combinations of hierarchy, inhibitor, reset and transfer arcs, except the termination problem for two combinations. For both these combinations, we show that deciding termination is as hard as deciding the positivity problem on linear recurrence sequences -- a long-standing open problem.
Cite as

S. Akshay, Supratik Chakraborty, Ankush Das, Vishal Jagannath, and Sai Sandeep. On Petri Nets with Hierarchical Special Arcs. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 40:1-40:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{akshay_et_al:LIPIcs.CONCUR.2017.40,
  author =	{Akshay, S. and Chakraborty, Supratik and Das, Ankush and Jagannath, Vishal and Sandeep, Sai},
  title =	{{On Petri Nets with Hierarchical Special Arcs}},
  booktitle =	{28th International Conference on Concurrency Theory (CONCUR 2017)},
  pages =	{40:1--40:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-048-4},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{85},
  editor =	{Meyer, Roland and Nestmann, Uwe},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.40},
  URN =		{urn:nbn:de:0030-drops-78026},
  doi =		{10.4230/LIPIcs.CONCUR.2017.40},
  annote =	{Keywords: Petri Nets, Hierarchy, Reachability, Coverability, Termination, Positivity}
}
Document
Complete Volume
DOI: 10.4230/LIPIcs.FSTTCS.2011
LIPIcs, Volume 13, FSTTCS'11, Complete Volume

Authors: Supratik Chakraborty and Amit Kumar

Published in: LIPIcs, Volume 13, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011)

Abstract
LIPIcs, Volume 13, FSTTCS'11, Complete Volume
Cite as

IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011). Leibniz International Proceedings in Informatics (LIPIcs), Volume 13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@Proceedings{chakraborty_et_al:LIPIcs.FSTTCS.2011,
  title =	{{LIPIcs, Volume 13, FSTTCS'11, Complete Volume}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011)},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-34-7},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{13},
  editor =	{Chakraborty, Supratik and Kumar, Amit},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2011},
  URN =		{urn:nbn:de:0030-drops-41077},
  doi =		{10.4230/LIPIcs.FSTTCS.2011},
  annote =	{Keywords: Software/Program Verification, Models of Computation, Modes of Computation, Complexity Measures and Classes, Nonnumerical Algorithms and Problems Specifying and Verifying and Reasoning about Programs}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.FSTTCS.2011.i
Frontmatter, Table of Contents, Preface, Conference Organization, External Reviewers

Authors: Supratik Chakraborty and Amit Kumar

Published in: LIPIcs, Volume 13, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011)

Abstract
Frontmatter, Table of Contents, Preface, Conference Organization, External Reviewers
Cite as

IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011). Leibniz International Proceedings in Informatics (LIPIcs), Volume 13, pp. i-xv, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{chakraborty_et_al:LIPIcs.FSTTCS.2011.i,
  author =	{Chakraborty, Supratik and Kumar, Amit},
  title =	{{Frontmatter, Table of Contents, Preface, Conference Organization, External Reviewers}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011)},
  pages =	{i--xv},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-34-7},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{13},
  editor =	{Chakraborty, Supratik and Kumar, Amit},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2011.i},
  URN =		{urn:nbn:de:0030-drops-33196},
  doi =		{10.4230/LIPIcs.FSTTCS.2011.i},
  annote =	{Keywords: Frontmatter, Table of Contents, Preface, Conference Organization, External Reviewers}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2011.xvi
Author Index

Authors: Supratik Chakraborty and Amit Kumar

Published in: LIPIcs, Volume 13, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011)

Abstract
Author Index
Cite as

Supratik Chakraborty and Amit Kumar. Author Index. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011). Leibniz International Proceedings in Informatics (LIPIcs), Volume 13, pp. 16-17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{chakraborty_et_al:LIPIcs.FSTTCS.2011.xvi,
  author =	{Chakraborty, Supratik and Kumar, Amit},
  title =	{{Author Index}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011)},
  pages =	{16--17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-34-7},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{13},
  editor =	{Chakraborty, Supratik and Kumar, Amit},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2011.xvi},
  URN =		{urn:nbn:de:0030-drops-33636},
  doi =		{10.4230/LIPIcs.FSTTCS.2011.xvi},
  annote =	{Keywords: Author Index}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact